A:Realizer, ds:x:Id fp Type, i, x:Id, T, T':Type, k:Knd, f:(State(x : T  ds)T'T).
R-Feasible(A)
 x  dom(R-state(A;i))
 ds || R-state(A;i)
 (isrcv(k)  R-da(A;source(lnk(k)))(k)?Void  T')
 (k  dom(R-da(A;i))  T' = Valtype(R-da(A;i);k))
 write-restricted(A;i;k)
 (y:Id. y  dom(x : T  ds)  read-restricted(A; i; y))
 @i effect k(v:T')  x := f State(x : T  ds) v  || A 

latex

Definitions

x:A. B(x), P  Q, A || B, Prop, DeclaredType(ds;x), {T}, x. t(x), t  T, Top, S  T, S  T, if b t else f fi, 1of(t), p  q, false, Y, True, Rplus?(x1), P & Q, Rplus-left(x1), Rplus-right(x1), Rnone?(x1), R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), p  q, i=j, 2of(t), true, Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), let x = a in b(x), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1), P  Q, P  Q, SQType(T), A & B, T, P  Q, A, Valtype(da;k), f(x)?z, write-restricted(R;i;k), read-restricted(R; i; y), Knd, b, x  dom(f), R-state(R;i), R-da(R;i), x(s), , , deq-member(eq;x;L), reduce(f;k;as), False, Unit, R-Feasible(R), f || g,

Lemmas

es realizer-induction, fpf wf, Id wf, Knd wf, decl-state wf, fpf-join wf, fpf-single wf, id-deq wf, R-Feasible wf, not wf, assert wf, fpf-dom wf, R-state wf, fpf-trivial-subtype-top, top wf, fpf-compatible wf, isrcv wf, subtype rel wf, fpf-cap wf, R-da wf, lsrc wf, lnk wf, Kind-deq wf, ma-valtype wf, write-restricted wf, read-restricted wf, R-compat wf, Reffect wf, fpf-cap-single-join, es realizer wf, Rnone wf, eq id wf, bool wf, iff transitivity, eqtt to assert, assert-eq-id, Id sq, eq id self, not functionality wrt iff, fpf-single-dom, fpf-compatible-join2, fpf-compatible-singles, fpf-empty-compatible-right, bnot wf, eqff to assert, assert of bnot, Rinit wf, Rframe wf, Rsframe wf, IdLnk wf, implies functionality wrt iff, band wf, eq knd wf, assert of band, and functionality wrt iff, assert-eq-knd, squash wf, true wf, fpf-cap-single1, fpf-compatible-single2, bor wf, bnot thru band, assert of bor, or functionality wrt iff, decl-type wf, fpf-compatible-join, lnk-decl wf, Knd sq, fpf-compatible-symmetry, lnk-decl-compatible-single, assert-eq-lnk, tagof wf, eq lnk wf, Rsends wf, locl wf, Rpre wf, Raframe wf, Rbframe wf, Rrframe wf, fpf-join-cap-sq, R-compat-Rplus2, all functionality wrt iff, R-compat-state, fpf-compatible-join-iff, fpf-join-dom, subtype rel transitivity, subtype-fpf-cap-void, fpf-sub-join-left, fpf-sub-join-right, R-compat-da, R-Feasible-effect, isrcv-implies, IdLnk sq, lnk-decl-dom, bool cases, bool sq, lnk-decl-cap